Mark Aagaard, PEng

Mark Aagaard is an Associate Professor in the Department of Electrical and Computer Engineering at the University of Waterloo.

His research interests include formal methods for the design and verification of digital-hardware systems. He has developed a formal theory for pipelined circuits based on the conventional ideas of structural hazards, control hazards, data hazards and datapath functionality. Dr. Aagaard’s current research activities use different formalization aspects of pipeline hazards to explore new design and verification techniques for varying classes of hazards.

Some recent projects of Dr. Aagaard’s include verifying data-hazard accuracy, exploiting the power and usability of an off-the-shelf combinational equivalence checker, and developing a prototype design and verification tool that includes a cell library of control components for pipeline stages. Dr. Aagaard also took part in creating the Microbox framework for microprocessor correctness statements, where over 30 published verification results were analyzed and proved correctness statement conditions.

• Formal verification

• Design and verification of digital hardware systems

• Computer architecture

• Computer & software engineering

• Connectivity and Internet of Things

• Wireless communications and networks

• Cybersecurity

• Application security

• Information security

• Infrastructure integrity

• Network security

• IoT (Internet of Things)

• Devices

• Application domains

• Dependability and security

• 1994, Doctorate Electrical Engineering, Cornell University, United States

• 1991, Master of Science Electrical Engineering, Cornell University, United States

• 1988, Bachelor of Science (BS) Electrical Engineering, Harvey Mudd College, United States

• ECE 108 - Discrete Mathematics and Logic 1
  • Taught in 2024, 2025
• ECE 208 - Discrete Mathematics and Logic 2
  • Taught in 2024
• ECE 327 - Digital Hardware Systems
  • Taught in 2020
• ECE 627 - Register-transfer-level Digital Systems
  • Taught in 2020

* Only courses taught in the past 5 years are displayed.

• Khalvati, Farzad and Aagaard, Mark D and Tizhoosh, Hamid R, Window memoization: toward high-performance image processing software, Journal of Real-Time Image Processing, 5, 2015

• Yang, Gangqiang and Aagaard, Mark D and Gong, Guang, Efficient Hardware Implementations of the Warbler Pseudorandom Number Generator, , , 2015

• O'Leary, John and Linderman, Mark and Leeser, Miriam and Aagaard, Mark, HML: A Hardware Description Language, Computer Hardware Description Languages and their Applications: Proceedings of the 11th IFIP WG10. 2 International Conference on Computer Hardware Description Languages and their Applications-CHDL'93 Sponsored by IFIP WG10. 2 and in cooperation with , 327, 2014

• Aagaard, Mark and Leeser, Miriam, A methodology for reusable hardware proofs, Proceedings of the IFIP TC10/WG10, 177, 2014

• Mandal, Kalikinkar and Gong, Guang and Fan, Xinxin and Aagaard, Mark, Optimal parameters for the WG stream cipher family, Cryptography and Communications, 117, 2014